$\vdash$${\it es}$.$P$(${\it es}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$R$:Realizer. $R$ $\Vdash$ ${\it es}$.$P$(${\it es}$)